Skip to content

Parallel branch verification#634

Merged
marcoeilers merged 36 commits into
masterfrom
meilers_parallel_branches
Sep 2, 2022
Merged

Parallel branch verification#634
marcoeilers merged 36 commits into
masterfrom
meilers_parallel_branches

Conversation

@marcoeilers

@marcoeilers marcoeilers commented Aug 11, 2022

Copy link
Copy Markdown
Contributor

(Depends on the Z3 API PR (not because there are real functional dependencies but simply because I merged the two at some point to be able to test both together))

Building on Malte's earlier attempt to get parallel branch verification, this PR adds a command line parameter --parallelizeBranches that directs Silicon to verify different branches in parallel.
We use a ForkJoinPool for this which uses a work stealing algorithm, so every worker has its own Z3 instance and its own work queue. When it reaches a branch, it puts the else-branch into its own queue s.t. other idle workers can take it; if noone does, it will take the else-branch-task from the beginning of its own queue and verify it itself.
Workers that become idle will steal from the end of the queue of another worker and therefore get the oldest task that worker still has left over, which tends to be the biggest task in the queue, which should avoid switching back and forth between workers for tiny tasks.
Every task switch requires updating the worker's solver to the branch's current state, i.e., popping all its current path conditions and pushing all path conditions from the task it's taking over.

Speedups obviously depend on the program and the machine, but if you have a bunch of cores lying around and your program has lots of branching, things will become MUCH faster (e.g. 6x for Nagini VerifyThis examples on my desktop at home).

@mschwerhoff mschwerhoff left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I totally approve on branch parallelisation 👍 💯 🥇 🚀 💎 But please see my comments nonetheless.

Comment thread src/main/scala/decider/Decider.scala Outdated
Comment thread src/main/scala/decider/Decider.scala
Comment thread src/main/scala/decider/PathConditions.scala Outdated
Comment thread src/main/scala/decider/ProverStdIO.scala Outdated
Comment thread src/main/scala/decider/Z3ProverAPI.scala Outdated
Comment thread src/main/scala/decider/Z3ProverAPI.scala Outdated
Comment thread src/main/scala/decider/Z3ProverAPI.scala Outdated
Comment thread src/main/scala/rules/Brancher.scala
Comment thread src/main/scala/rules/Executor.scala Outdated
Comment thread src/main/scala/verifier/VerificationPoolManager.scala Outdated
@marcoeilers marcoeilers merged commit efda78c into master Sep 2, 2022
@marcoeilers marcoeilers deleted the meilers_parallel_branches branch September 2, 2022 14:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants